
%%%%%%%%%%%%%%%%%%%%%%% file typeinst.tex %%%%%%%%%%%%%%%%%%%%%%%%%
%
% This is the LaTeX source for the instructions to authors using
% the LaTeX document class 'llncs.cls' for contributions to
% the Lecture Notes in Computer Sciences series.
% http://www.springer.com/lncs       Springer Heidelberg 2006/05/04
%
% It may be used as a template for your own input - copy it
% to a new file with a new name and use it as the basis
% for your article.
%
% NB: the document class 'llncs' has its own and detailed documentation, see
% ftp://ftp.springer.de/data/pubftp/pub/tex/latex/llncs/latex2e/llncsdoc.pdf
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\documentclass[runningheads]{llncs}
\usepackage{txfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Modeling and Verification a PLC Design Pattern in Coq}

% a short form should be given in case it is too long for the running head
\titlerunning{}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{Hai Wan, Ming Gu, Xiaoyu Song}
%
\authorrunning{Hai Wan, Ming Gu, Xiaoyu Song}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{School of Software, Tsinghua University}


\toctitle{Modeling and Verification a PLC Design Pattern in Coq}
\tocauthor{Hai Wan} \maketitle


\begin{abstract}
In this paper, a translation from LTS to PLC is discussed. Through
analysis several flaws of the translation are disclosed. Due to the
flaws, a new translation method is proposed. The new translation is
modeled and verified using theorem prover Coq. Two key properties of
the new translation are proved which ensure its correctness. A
methodology of modeling and verifying PLC programs using theorem
prover is also given.
 \keywords{PLC, LTS, Theorem Proving, Coq}
\end{abstract}


\section{Introduction}

Labeled transition systems are commonly used in PLC designs. The
translation of LTS to PLC codes is of great importance.

\section{Discussion of the old translation}

Given a LTS $M = <S,S_{0},G,T>$, $S$ denotes for the states, $S_{0}$
denotes for the initial states, $G$ denotes for the labels(this will
be described as guards for convenience) on the edges and $T$ denotes
for the transitions. In practical the PLC design, there three
constraints on LTS:

\begin{enumerate}

\item There no self cycles in LTS, for the reason that self cycle
means the state of LTS is not changed which is of no use in PLC
programs.

\item There is only one initial state.

\item For every state, there must exist at least one path that through which it can
get back to the initial state, since the PLC programs are designed
to do job repeatedly and the job always starts at the initial state.

\end{enumerate}

For a LTS $M = <S,S_{0},G,T>$, the old translation method is
described as follows:

\begin{enumerate}

\item For any state $s$ in $S$, there is a SR flip-flop $M_{s}$ for
it.

\item For any guard $g$ in $G$, there is a relay $G_{g}$ for it.

\item The set condition of $M_{s}$ is: if there exists a $M_{s'}$ and a relay $G_{g}$ such that $<s',g,s> \in
T$ and the voltages of $M_{s'}$ and $G_{g}$ both are high.

\item The reset condition of $M_{s}$ is: if there exists a $M_{s'}$ such that
$s'$ is a successor of $s$ and the voltage of $M_{s'}$ is high.

\end{enumerate}

For example, the LTS in figure 1(a) can be translated to figure 1(b)
using this method.

\begin{figure}
\centering
\includegraphics[scale=0.95]{fig2}
\caption{A sample of translating a LTS to PLC codes.}
\label{fig:example}
\end{figure}

The translation of LTS should preserve the following two properties
of LTS:

\begin{enumerate}

\item In the translated PLC codes, the must be several relays that represent the state of the LTS. The number of these relays of high voltage should be one and only one at the end of every cycle.

\item The state should be change (if can change) only by one step forward. For
example, in figure 1 the current state is $s_{0}$ at cycle $i$, then
at cycle $i+1$ the state can only be $s_{0}$ or change to $s_{1}$.
It can not change to $s_{2}$ even if the guard $g_{1}$ and $g_{2}$
both are true.

\end{enumerate}

Under some conditions, using the translation described above can be
flauty. Take the LTS in figure 1 for instance, if $M_{1}$ and
$g_{1}$ are both high in the current scan cycle. $M_{1}$ is high
means that the LTS is at its state $s_{1}$. $g_{1}$ is high means
that the transition from $M_{1}$ to $M_{2}$ is enabled. It is
obvious that at the end of this scan cycle, $M_{1}$ and $M_{2}$ both
are high, which means that LTS is at its $s_{1}$ and $s_{2}$. It is
an error. In practice, engineers use mutex relays to prevent this
situation. But it is not a systematical way to solve this problem.
Intuitively we can move the SR flip-flop $M_{2}$ to the front of
$M_{1}$. The following theorem shows that we cannot solve the
problem by ordering the SR flip-flops.

\textbf{Theorem 1.} No matter what the order of the SR flip-flops
is, there exists some conditions under which two or more SR
flip-flops can be high at the end of the same cycle.

Omitted.

This fashion of translation also will break the law under some
special conditions. For example, if $M_{1}$, $g_{1}$ and $g_{2}$ are
high, then after one cycle $M_{3}$ will be high which break the
second property of translation.

\section{Description of the new translation}

According to the flaws of the existing translation, we designed a
new translation from LTS to PLC codes. The translation process is
described as below.

\begin{enumerate}

\item For every state $s$ in LTS, the set of its successor states is denoted by
$S'_{s}$. Every state in

\item For any state $s$ in $S$, there are two SR flip-flops $M_{s}$ and $M'_{s}$ for
it.

\item For any guard $g$ in $G$, there is a relay $G_{g}$ for it.

\item For every state $s$, copy the
 value of $M_{s}$ to $M'_{s}$ at the beginning of every scan cycle.

\item The set condition of $M'_{s}$ is: if there exists a $M'_{s'}$ and a relay $G_{g}$ such that $<s',g,s> \in
T$ and the voltages of $M_{s'}$ and $G_{g}$ both are high.

\item There are two reset conditions for $M'_{s}$:

\begin{enumerate}

\item $M'_{s}$ is high and there exists a $M'_{s'}$ and a relay $G_{g}$ such that $<s,g,s'> \in T$ and $M'_{s'}$ and
$G_{g}$ both are high.

\item There exists $M_{s_{1}}$, $M_{s_{2}}$, $G_{g_{1}}$, $G_{g_{2}}$ such that
$M_{s_{1}}$ is high, $G_{g_{1}}$ is high, $<s_{1},g_{1},s> \in T$,
$<s_{1},g_{2},s_{2}>\in T$ and the precedence of $s_{2}$ is higher
than $s$'s.

\end{enumerate}

\item After the calculation described above, copy $M'_{s}$ to
$M_{s}$ for every $s$ at the end of scan cycle.

\end{enumerate}

An example of the new transformation is demonstrated in figure 2.

\begin{figure}
\centering
\includegraphics[scale=0.7]{fig3}
\caption{An example of new transformation} \label{fig:example}
\end{figure}

\section{Modeling of the design pattern}

In this section, we show how the design pattern is modeled in Coq.

As described in the previous section, there are two kinds of relays
in our design: one represents the states of LTS, and the other
represents the guards. Due to the fact that the number of relays in
a PLC program must be finite, we define two upper bounds :
\emph{MaxNode} and \emph{MaxGuard}. And then two sorts are defined
accordingly : \emph{nodes} and \emph{guards}.

\begin{verbatim}
    Variable MaxNode : nat.
    Variable MaxGuard : nat.
    Definition nodes := {n|n<=MaxNode}.
    Definition guards : = {n|n<=MaxGuard}.
\end{verbatim}

All states of the system is denoted as the sort \emph{state}, whose
items are functions mapping from \emph{nodes} to \emph{Prop}. The
items of sort \emph{state} are arbitrary which means that there are
states whose values both are true. This condition is forbidden in
LTS. Another sort \emph{v\_state} is defined to denote the valid
states of the system, i.e., states of which just only one node's
value is true.

\begin{verbatim}
    Definition state := nodes -> Prop.
    Inductive v_state : state -> Prop :=
        vs_intro : forall s : state,
            (exists! n : nodes, s n) -> v_state s.
\end{verbatim}

Given a LTS $M = <S,G,T>$, \emph{Rss} and \emph{Rsgs} are used to
modeling $M$. Intuitively, if we have an item $<n_{1},g,n_{2}\
>\ \in T$, then we have $Rss\ n_{1}\ n_{2}\ =\ True$. \emph{Rsgs} is
a little more complex, in order to use $Rsgs$ we should provide a
proof $f$ that $n_{1}$ is the predecessor of $n_{2}$, and then we
can get $Rsgs\ n_{1}\ n_{2}\ f\ =\ g$.

\begin{verbatim}
    Variable Rss : nodes->nodes->Prop.
    Hypothesis Rsgs : forall n1 n2:nodes, Rss n1 n2 -> guards.
\end{verbatim}

The precedence of nodes is denoted by Pre, which means that given
three nodes $n_{1}, n_{2}$ and $n_{3}$, if $n_{2}$ and $n_{3}$ both
successors of $n_{1}$ and $n_{2}$'s precedence is higher than
$n_{3}$'s, then $Pre\ n_{1}\ n_{2}\ n_{3} = True$.

\begin{verbatim}
    Variable Pre : nodes->nodes->nodes->Prop.
\end{verbatim}

Variable \emph{Guard} is used to denoted the state of all guards.
Given a guard \emph{g}, \emph{Guard g} denotes the value of guard
\emph{g}.

\begin{verbatim}
    Variable Guard : guards->Prop.
\end{verbatim}

There several constraints or properties on \emph{Rss} and
\emph{Pre}. Hypothesis \emph{no\_self\_cycle} denotes that there is
no self cycles in the LTS \emph{M}. Hypothesis\emph{Pre\_1},
\emph{Pre\_2} and \emph{Pre\_3} means if nodes $n_{1}$ and $n_{2}$
are comparable, then they are both successors of $n_{1}$ and they
are not equal. Hypothesis \emph{Pre\_4} shows that if $n_{2}$ has
higher precedence than $n_{3}$, then $n_{3}$'s precedence is lower
than $n_{2}$'s. All of these hypothesis are straight forward.

\begin{verbatim}
    Hypothesis no_self_cycle : forall n, ~ Rss n n.
    Hypothesis Pre_1 :
        forall n1 n2 n3, Pre n1 n2 n3 -> Rss n1 n2.
    Hypothesis Pre_2 :
        forall n1 n2 n3, Pre n1 n2 n3 -> Rss n1 n3.
    Hypothesis Pre_3 :
        forall n1 n2 n3, Pre n1 n2 n3 -> n2 <> n3.
    Hypothesis Pre_4 :
        forall n1 n2 n3, Pre n1 n2 n3 -> ~ Pre n1 n3 n2.
\end{verbatim}

In Coq, the modeling of SR flip-flop is not straight forward. We use
another structure (shown in figure 3) to present SR flip-flop. Their
equivalence is easily proved. The Coq codes of next fuction of node
1 using the modeling framework described above is demonstrated
below.

\begin{figure}
\centering
\includegraphics[scale=0.5]{fig1}
\caption{A SR flip-flop in PLC. Node 0 is S, node 2 is R and node 1
is the output of SR flip-flop.} \label{fig:example}
\end{figure}

\begin{verbatim}
    Definition Next_2 (s : state) : Prop :=
        (s 0 \/ s 1) /\ ~ s 2.
\end{verbatim}

The Coq codes below is the function how we calculate the next state
based on the current state. These codes are divided into three
parts, each part corresponds with the conditions mentioned in
section 3.

\begin{enumerate}

\item \textbf{Set condition:}

''$(s\ n \vee (exists\ n', exists\ H, n'<>n \wedge s\ n' \wedge
Guard\ (Rsgs\ n'\ n\ H)))$'' means the result value of node $n$ is
$True$ if the current value of $n$ is $True$ or there exists a
predecessor $n'$ of $n$ whose value and the guard of $n$ and $n'$
are both $True$.

\item \textbf{Reset condition 1}:

''$\sim(s\ n \wedge exists\ n', exists\ H, n<>n' \wedge Guard\
(Rsgs\ n\ n'\ H))$'' means if $n$'s current value is $True$ and
there exists a successor $n'$ of $n$ and the guard of $n$ and $n'$
is $True$, then the value of $n$ is set to $False$.

\item \textbf{Reset condition 2}:

''$\sim(exists\ n', exists\ n'', exists\ H,n' <> n \wedge s\ n''
\wedge Rss\ n''\ n \wedge Pre\ n''\ n'\ n\wedge Guard\ (Rsgs\ n''\
n'\ H))$'' means if there exists a $n'$ such that it has the same
predecessor of $n$, its precedence is higher than $n$ and its guard
condition is $True$, then $n$'s value is set to $False$.

\end{enumerate}

\begin{verbatim}
Definition Next (s : state) : state :=
    fun (n:nodes) =>
        (s n \/ (exists n', exists H, n'<>n /\ s n' /\
            Guard (Rsgs n' n H)))
        /\
        ~(s n /\ exists n', exists H, n<>n' /\ Guard (Rsgs n n' H))
        /\
        ~(exists n', exists n'', exists H,
            n' <> n /\ s n'' /\ Rss n'' n /\ Pre n'' n' n
            /\ Guard (Rsgs n'' n' H)).
\end{verbatim}

\section{Verification of the design pattern}

The two critical properties of the translation from LTS to PLC
programs are list below. They ensure the absence of the two flaws
described in section 2.

\textbf{Property 1}: If the current state is valid then the next
state calculated by the $Next$ function is also valid.

\textbf{Property 2}: If the current state $s$ is valid, $x$ is the
node whose value is $True$, and in the next state the node $x'$ is
of value $True$, then either $x$ equals $x'$ or $x$ is the successor
of $x'$.

\begin{verbatim}
Theorem RelationNext :
    forall s, v_state s -> forall x, s x -> forall x',
        (Next s) x' -> x = x' \/ Rss x x'.

Theorem FromValid_is_Valid :
    forall s:state, v_state s -> v_state (Next s).

\end{verbatim}

In order to prove this, we first introduce a function $GetMax$.
Given a node $n_{1}$ and a proof that there exists a successor
$n_{2}$ of $n_{1}$ such that the guard between $n_{1}$ and $n_{2}$
is $True$, we can using $GetMax$ to get the node of the highest
precedence. The properties the function $GetMax$ are hold are also
list below.

\begin{verbatim}
Hypothesis GetMax :
    forall n, (exists n', exists H:Rss n n',
        Guard(Rsgs n n' H))-> nodes.
Hypothesis GetMax_property_1 :
    forall n1 n2 H, Rss n1 n2 -> Pre n1 (GetMax n1 H) n2.
Hypothesis GetMax_property_2 :
    forall n1 H1 H, Guard (Rsgs n1 (GetMax n1 H1) H).
Hypothesis GetMax_property_3 :
    forall n1 H, GetMax n1 H <> n1.
Hypothesis GetMax_property_4 :
    forall n1 n2 H, Rss n1 n2 -> (GetMax n1 H = n2 \/ GetMax n1 H <> n2).
Hypothesis GetMax_property_5 :
    forall n1 H, Rss n1 (GetMax n1 H).
\end{verbatim}

First we proved the lemma $AllNotTrue\_or\_SomeAreTrue$, which means
for any node either condition that all guards of its outgoing edges
are $False$, or condition that some guards of its outgoing edges are
$True$ is held. If the first condition is held This can be easily
proved. But in Coq we do not have the excluded middle law, the
Classical library should be import first. Based on lemma
$AllNotTrue\_or\_SomeAreTrue$, hypothesis of function $GetMax$ and
function $Pre$, the two properties can be proved.

\begin{verbatim}
Lemma AllNotTrue_or_SomeAreTrue :
    forall n, (forall n' H, ~ Guard (Rsgs n n' H)) \/
        (exists n', exists H, Guard (Rsgs n n' H)).
\end{verbatim}



\section{Conclusion}


\begin{thebibliography}{4}



\end{thebibliography}


\end{document}
